1 /-
2 Copyright (c) 2018 Chris Hughes. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Chris Hughes
5
6 Definition of splitting fields, and definition of homomorphism into any field that splits
7 -/
8
9 import ring_theory.unique_factorization_domain
src └─────────────────────────────────────┘
10 import data.polynomial ring_theory.principal_ideal_domain
src └─────────────┘ └────────────────────────────────┘
11 algebra.euclidean_domain
src └──────────────────────┘
12
13 local attribute [instance, priority 100000] is_ring_hom.id
14
15 universes u v w
16
17 variables {α : Type u} {β : Type v} {γ : Type w}
18
19 namespace polynomial
20
21 noncomputable theory
22 open_locale classical
23 variables [discrete_field α] [discrete_field β] [discrete_field γ]
id └────────────┘ └────────────┘ └────────────┘
src └────────────┘ └────────────┘ └────────────┘
typ └────────────┘ └────────────┘ └────────────┘
24 open polynomial
25
26 section splits
27
28 variables (i : α → β) [is_ring_hom i]
id └─────────┘
src └─────────┘
typ └─────────┘
doc └─────────┘
29
30 /-- a polynomial `splits` iff it is zero or all of its irreducible factors have `degree` 1 -/
31 def splits (f : polynomial α) : Prop :=
id └────────┘ ┴
src └────────┘
typ └────────┘ ┴
doc └────────┘
32 f = 0 ∨ ∀ {g : polynomial β}, irreducible g → g ∣ f.map i → degree g = 1
id ┴ ┴ ┴ └────────┘ ┴ └─────────┘ ┴ ┴ ┴ ┴└──┘ ┴ └────┘ ┴ ┴
src ┴ ┴ └────────┘ └─────────┘ ┴ └──┘ └────┘ ┴
typ ┴ ┴ ┴ └────────┘ ┴ └─────────┘ ┴ ┴ ┴ ┴└──┘ ┴ └────┘ ┴ ┴
doc └────────┘ └─────────┘ └──┘ └────┘
33
34 @[simp] lemma splits_zero : splits i (0 : polynomial α) := or.inl rfl
id └────┘ ┴ └────────┘ ┴ └────┘ └─┘
src └────┘ └────────┘ └────┘ └─┘
typ └────┘ ┴ └────────┘ ┴ └────┘ └─┘
doc └──┘ └────┘ └────────┘
35
36 @[simp] lemma splits_C (a : α) : splits i (C a) :=
id ┴ └────┘ ┴ ┴ ┴
src └────┘ ┴
typ ┴ └────┘ ┴ ┴ ┴
doc └──┘ └────┘ ┴
37 if ha : a = 0 then ha.symm ▸ (@C_0 α _).symm ▸ splits_zero i
id └─┘ └─────────┘
src └─┘ └─────────┘
typ └─┘ └─────────┘
38 else
39 have hia : i a ≠ 0, from mt ((is_add_group_hom.injective_iff i).1
id └┘ └────────────────────────────┘
src └┘ └────────────────────────────┘
typ └┘ └────────────────────────────┘
40 (is_ring_hom.injective i) _) ha,
id └───────────────────┘
src └───────────────────┘
typ └───────────────────┘
41 or.inr $ λ g hg ⟨p, hp⟩, absurd hg.1 (classical.not_not.2 (is_unit_iff_degree_eq_zero.2 $
id └────┘ └────┘ └───────────────┘ └────────────────────────┘
src └────┘ └────┘ └───────────────┘ └────────────────────────┘
typ └────┘ └────┘ └───────────────┘ └────────────────────────┘
42 by have := congr_arg degree hp;
src └──────┘ ┴ ┴
typ └──────┘ ┴ ┴
doc └──────┘ ┴ ┴
txt └──────┘ ┴ ┴
par └──────┘ ┴ ┴
pid └───┘└─┘ ┴ ┴
43 simp [degree_C hia, @eq_comm (with_bot ℕ) 0,
src └────┘ ┴ └┘ ┴ ┴ └────
typ └────┘ ┴ └┘ ┴ ┴ └────
doc └────┘ ┴ └┘ ┴ ┴ └────
txt └────┘ ┴ └┘ ┴ ┴ └────
par └────┘ ┴ └┘ ┴ ┴ └────
pid ┴┴ ┴ └┘ ┴ ┴ └────
44 nat.with_bot.add_eq_zero_iff] at this; clear _fun_match; tautology))
id └───────────────────────┘
src ─────┘ └───────────────────────┘└───────┘ └──────────────┘ └───────┘
typ ─────┘ └───────────────────────┘└───────┘ └──────────────┘ └───────┘
doc ─────┘ └───────┘ └──────────────┘ └───────┘
txt ─────┘ └───────┘ └──────────────┘ └───────┘
par ─────┘ └───────┘ └──────────────┘ └───────┘
pid ─────┘ ┴┴└─────┘ └─────────┘
st └─────────────────────────────────────────────────────────────┘
45
46 lemma splits_of_degree_eq_one {f : polynomial α} (hf : degree f = 1) : splits i f :=
id └────────┘ ┴ └────┘ ┴ ┴ └────┘ ┴ ┴
src └────────┘ └────┘ ┴ └────┘
typ └────────┘ ┴ └────┘ ┴ ┴ └────┘ ┴ ┴
doc └────────┘ └────┘ └────┘
47 or.inr $ λ g hg ⟨p, hp⟩,
id └────┘ ┴ └┘ ┴
src └────┘
typ └────┘ ┴ └┘ ┴
48 by have := congr_arg degree hp;
id └───────┘ └────┘ └┘
src └──────┘└───────┘┴└────┘┴
typ └──────┘└───────┘┴└────┘┴└┘
doc └──────┘ ┴└────┘┴
txt └──────┘ ┴ ┴
par └──────┘ ┴ ┴
pid └───┘└─┘ ┴ ┴
st └─────────────────────────────
49 simp [nat.with_bot.add_eq_one_iff, hf, @eq_comm (with_bot ℕ) 1,
id └─────────────────────────┘ └┘ └─────┘ └──────┘
src └────┘└─────────────────────────┘└┘ └┘ └─────┘┴ └──────┘┴ └────
typ └────┘└─────────────────────────┘└┘└┘└┘ └─────┘┴ └──────┘┴ └────
doc └────┘ └┘ └┘ ┴ ┴ └────
txt └────┘ └┘ └┘ ┴ ┴ └────
par └────┘ └┘ └┘ ┴ ┴ └────
pid ┴┴ └┘ └┘ ┴ ┴ └────
st ──────────────────────────────────────────────────────────────────
50 mt is_unit_iff_degree_eq_zero.2 hg.1] at this;
id └┘ └────────────────────────┘ └┘
src ───┘└┘┴└────────────────────────┘└─┘ └─────────┘
typ ───┘└┘┴└────────────────────────┘└─┘└┘└─────────┘
doc ───┘ ┴ └─┘ └─────────┘
txt ───┘ ┴ └─┘ └─────────┘
par ───┘ ┴ └─┘ └─────────┘
pid ───┘ ┴ └─┘ └─┘┴└─────┘
st ───────────────────────────────────────────────────
51 clear _fun_match; tauto
src └──────────────┘ └─────
typ └──────────────┘ └─────
doc └──────────────┘ └─────
txt └──────────────┘ └─────
par └──────────────┘ └─────
pid └─────────┘ └
st ──────────────────────────
52
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
53 lemma splits_of_degree_le_one {f : polynomial α} (hf : degree f ≤ 1) : splits i f :=
id └────────┘ ┴ └────┘ ┴ ┴ └────┘ ┴ ┴
src └────────┘ └────┘ ┴ └────┘
typ └────────┘ ┴ └────┘ ┴ ┴ └────┘ ┴ ┴
doc └────────┘ └────┘ └────┘
54 begin
st └─────
55 cases h : degree f with n,
id └────┘ ┴
src └────┘ └─┘└────┘┴ └─────┘
typ └────┘ └─┘└────┘┴┴└─────┘
doc └────┘ └─┘└────┘┴ └─────┘
txt └────┘ └─┘ ┴ └─────┘
par └────┘ └─┘ ┴ └─────┘
pid ┴ └─┘ ┴ └─────┘
st ──────────────────────────┘└─
56 { rw [degree_eq_bot.1 h]; exact splits_zero i },
id └───────────┘ ┴ └─────────┘ ┴
src └──┘└───────────┘└─┘ ┴ └────┘└─────────┘┴ ┴
typ └──┘└───────────┘└─┘┴┴ └────┘└─────────┘┴┴┴
doc └──┘ └─┘ ┴ └────┘ ┴ ┴
txt └──┘ └─┘ ┴ └────┘ ┴ ┴
par └──┘ └─┘ ┴ └────┘ ┴ ┴
pid └┘ └─┘ ┴ ┴ ┴ ┴
st ───┘└───────────────────┘┴└────────────────────┘└┘└
57 { cases n with n,
id ┴
src └────┘ └─────┘
typ └────┘┴└─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴ └─────┘
st ─────────────────┘└─
58 { rw [eq_C_of_degree_le_zero (trans_rel_right (≤) h (le_refl _))];
id └────────────────────┘ └─────────────┘ ┴ ┴ └─────┘
src └──┘└────────────────────┘┴ └─────────────┘┴┴└─┘ ┴ └─────┘└───┘
typ └──┘└────────────────────┘┴ └─────────────┘┴┴└─┘┴┴ └─────┘└───┘
doc └──┘ ┴ ┴ └─┘ ┴ └───┘
txt └──┘ ┴ ┴ └─┘ ┴ └───┘
par └──┘ ┴ ┴ └─┘ ┴ └───┘
pid └┘ ┴ ┴ └─┘ ┴ └───┘
st ─────┘└────────────────────────────────────────────────────────────┘┴└─
59 exact splits_C _ _ },
id └──────┘
src └────┘└──────┘└───┘
typ └────┘└──────┘└───┘
doc └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ └──┘┴
st ────────────────────────┘└┘└
60 { have hn : n = 0,
id ┴
src └────────┘ ┴ └┘
typ └────────┘┴┴ └┘
doc └────────┘ ┴ └┘
txt └────────┘ ┴ └┘
par └────────┘ ┴ └┘
pid └─────┘└─┘ ┴ ┴┴
st ────────────────────┘└─
61 { rw h at hf,
id ┴
src └─┘ └────┘
typ └─┘┴└────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ └────┘
st ───────┘└────────┘└─
62 cases n, { refl }, { exact absurd hf dec_trivial } },
id ┴ └────┘ └┘ └─────────┘
src └────┘ └───┘ └────┘└────┘┴ ┴└─────────┘┴
typ └────┘┴ └───┘ └────┘└────┘┴└┘┴└─────────┘┴
doc └────┘ └───┘ └────┘ ┴ ┴└─────────┘┴
txt └────┘ └───┘ └────┘ ┴ ┴ ┴
par └────┘ └───┘ └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────┘└──┘└───┘└┘└─────────────────────────────┘└──┘└
63 exact splits_of_degree_eq_one _ (by rw [h, hn]; refl) } }
id └─────────────────────┘ ┴ └┘
src └────┘└─────────────────────┘└─┘ ┴└──┘ └┘ ┴└┘└──┘└┘
typ └────┘└─────────────────────┘└─┘ ┴└──┘┴└┘└┘┴└┘└──┘└┘
doc └────┘ └─┘ ┴└──┘ └┘ ┴└┘└──┘└┘
txt └────┘ └─┘ ┴└──┘ └┘ ┴└┘└──┘└┘
par └────┘ └─┘ ┴└──┘ └┘ ┴└┘└──┘└┘
pid ┴ └─┘ └───┘ └┘ └──────┘┴
st ────────────────────────────────────────┘└────┘└──┘┴└────┘└┘└───
64 end
st ──┘
65
66 lemma splits_mul {f g : polynomial α} (hf : splits i f) (hg : splits i g) : splits i (f * g) :=
id └────────┘ ┴ └────┘ ┴ ┴ └────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴
src └────────┘ └────┘ └────┘ └────┘ ┴
typ └────────┘ ┴ └────┘ ┴ ┴ └────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴
doc └────────┘ └────┘ └────┘ └────┘
67 if h : f * g = 0 then by simp [h]
id └┘ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ ┴ └────┘ └┘
typ └┘ ┴ ┴ ┴ ┴ └────┘┴└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st └────────┘
68 else or.inr $ λ p hp hpf, ((principal_ideal_domain.irreducible_iff_prime.1 hp).2.2 _ _
id └────┘ ┴ ┴ └┘ └─┘ └──────────────────────────────────────────┘┴ └┘ ┴ ┴
src └────┘ └──────────────────────────────────────────┘┴ ┴ ┴
typ └────┘ ┴ ┴ └┘ └─┘ └──────────────────────────────────────────┘┴ └┘ ┴ ┴
69 (show p ∣ map i f * map i g, by convert hpf; rw polynomial.map_mul)).elim
id ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ └────────────────┘ └──┘
src ┴ └─┘ ┴ └─┘ └──────┘ └─┘└────────────────┘ └──┘
typ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └──────┘└─┘ └─┘└────────────────┘ └──┘
doc └─┘ └─┘ └──────┘ └─┘
txt └──────┘ └─┘
par └──────┘ └─┘
pid ┴ ┴
st └───────────────┘└────────────────┘
70 (hf.resolve_left (λ hf, by simpa [hf] using h) hp)
id └┘└───────────┘ └┘ └┘ ┴ └┘
src └───────────┘ └─────┘ └──────┘
typ └┘└───────────┘ └┘ └─────┘└┘└──────┘┴ └┘
doc └─────┘ └──────┘
txt └─────┘ └──────┘
par └─────┘ └──────┘
pid ┴┴ ┴┴└────┘
st └─────────────────┘
71 (hg.resolve_left (λ hg, by simpa [hg] using h) hp)
id └┘└───────────┘ └┘ └┘ ┴ └┘
src └───────────┘ └─────┘ └──────┘
typ └┘└───────────┘ └┘ └─────┘└┘└──────┘┴ └┘
doc └─────┘ └──────┘
txt └─────┘ └──────┘
par └─────┘ └──────┘
pid ┴┴ ┴┴└────┘
st └─────────────────┘
72
73 lemma splits_of_splits_mul {f g : polynomial α} (hfg : f * g ≠ 0) (h : splits i (f * g)) :
id └────────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴
src └────────┘ ┴ ┴ └────┘ ┴
typ └────────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴
doc └────────┘ └────┘
74 splits i f ∧ splits i g :=
id └────┘ ┴ ┴ ┴ └────┘ ┴ ┴
src └────┘ ┴ └────┘
typ └────┘ ┴ ┴ ┴ └────┘ ┴ ┴
doc └────┘ └────┘
75 ⟨or.inr $ λ g hgi hg, or.resolve_left h hfg hgi (by rw map_mul; exact dvd.trans hg (dvd_mul_right _ _)),
id └────┘ ┴ └─┘ └┘ └─────────────┘ ┴ └─┘ └─┘ └─────┘ └───────┘ └┘ └───────────┘
src └────┘ └─────────────┘ └─┘└─────┘ └────┘└───────┘┴ ┴ └───────────┘└───┘
typ └────┘ ┴ └─┘ └┘ └─────────────┘ ┴ └─┘ └─┘ └─┘└─────┘ └────┘└───────┘┴└┘┴ └───────────┘└───┘
doc └─┘ └────┘ ┴ ┴ └───┘
txt └─┘ └────┘ ┴ ┴ └───┘
par └─┘ └────┘ ┴ ┴ └───┘
pid ┴ ┴ ┴ ┴ └───┘
st └─────────────────────────────────────────────────┘
76 or.inr $ λ g hgi hg, or.resolve_left h hfg hgi (by rw map_mul; exact dvd.trans hg (dvd_mul_left _ _))⟩
id └────┘ ┴ └─┘ └┘ └─────────────┘ ┴ └─┘ └─┘ └─────┘ └───────┘ └┘ └──────────┘
src └────┘ └─────────────┘ └─┘└─────┘ └────┘└───────┘┴ ┴ └──────────┘└───┘
typ └────┘ ┴ └─┘ └┘ └─────────────┘ ┴ └─┘ └─┘ └─┘└─────┘ └────┘└───────┘┴└┘┴ └──────────┘└───┘
doc └─┘ └────┘ ┴ ┴ └───┘
txt └─┘ └────┘ ┴ ┴ └───┘
par └─┘ └────┘ ┴ ┴ └───┘
pid ┴ ┴ ┴ ┴ └───┘
st └────────────────────────────────────────────────┘
77
78 lemma splits_map_iff (j : β → γ) [is_ring_hom j] {f : polynomial α} :
id ┴ ┴ └─────────┘ ┴ └────────┘ ┴
src └─────────┘ └────────┘
typ ┴ ┴ └─────────┘ ┴ └────────┘ ┴
doc └─────────┘ └────────┘
79 splits j (f.map i) ↔ splits (λ x, j (i x)) f :=
id └────┘ ┴ ┴└──┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
src └────┘ └──┘ ┴ └────┘
typ └────┘ ┴ ┴└──┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
doc └────┘ └──┘ └────┘
80 by simp [splits, polynomial.map_map]
id └────┘ └────────────────┘
src └────┘└────┘└┘└────────────────┘└─
typ └────┘└────┘└┘└────────────────┘└─
doc └────┘└────┘└┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └──────────────────────────────────
81
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
82 lemma exists_root_of_splits {f : polynomial α} (hs : splits i f) (hf0 : degree f ≠ 0) :
id └────────┘ ┴ └────┘ ┴ ┴ └────┘ ┴ ┴
src └────────┘ └────┘ └────┘ ┴
typ └────────┘ ┴ └────┘ ┴ ┴ └────┘ ┴ ┴
doc └────────┘ └────┘ └────┘
83 ∃ x, eval₂ i x f = 0 :=
id ┴ ┴┴ └───┘ ┴ ┴ ┴ ┴
src ┴ ┴ └───┘ ┴
typ ┴ ┴┴ └───┘ ┴ ┴ ┴ ┴
doc └───┘
84 if hf0 : f = 0 then ⟨37, by simp [hf0]⟩
id └┘ ┴ ┴ └─┘
src └┘ ┴ └────┘ ┴
typ └┘ ┴ ┴ └────┘└─┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st └─────────┘
85 else
86 let ⟨g, hg⟩ := is_noetherian_ring.exists_irreducible_factor
id └─┘ └┘ └──────────────────────────────────────────┘
src └──────────────────────────────────────────┘
typ └─┘ └┘ └──────────────────────────────────────────┘
87 (show ¬ is_unit (f.map i), from mt is_unit_iff_degree_eq_zero.1 (by rwa degree_map))
id ┴ └─────┘ ┴└──┘ ┴ └┘ └────────────────────────┘┴ └────────┘
src ┴ └─────┘ └──┘ └┘ └────────────────────────┘┴ └──┘└────────┘
typ ┴ └─────┘ ┴└──┘ ┴ └┘ └────────────────────────┘┴ └──┘└────────┘
doc └─────┘ └──┘ └──┘
txt └──┘
par └──┘
pid ┴
st └─────────────┘
88 (by rw [ne.def, map_eq_zero]; exact hf0) in
id └────┘ └─────────┘ └─┘
src └──┘└────┘└┘└─────────┘┴ └────┘
typ └──┘└────┘└┘└─────────┘┴ └────┘└─┘
doc └──┘ └┘ ┴ └────┘
txt └──┘ └┘ ┴ └────┘
par └──┘ └┘ ┴ └────┘
pid └┘ └┘ ┴ ┴
st └─────────┘└───────────┘┴└─────────┘
89 let ⟨x, hx⟩ := exists_root_of_degree_eq_one (hs.resolve_left hf0 hg.1 hg.2) in
id └─┘ ┴ └──────────────────────────┘ └┘└───────────┘ └─┘ ┴ ┴
src └──────────────────────────┘ └───────────┘ ┴ ┴
typ └─┘ ┴ └──────────────────────────┘ └┘└───────────┘ └─┘ ┴ ┴
90 let ⟨i, hi⟩ := hg.2 in
id └─┘ ┴
src ┴
typ └─┘ ┴
91 ⟨x, by rw [← eval_map, hi, eval_mul, show _ = _, from hx, zero_mul]⟩
id └──────┘ └┘ └──────┘ ┴ └┘ └──────┘
src └────┘└──────┘└┘ └┘└──────┘└┘ └─┘┴└───────┘ └┘└──────┘┴
typ └────┘└──────┘└┘└┘└┘└──────┘└┘ └─┘┴└───────┘└┘└┘└──────┘┴
doc └────┘ └┘ └┘ └┘ └─┘ └───────┘ └┘ ┴
txt └────┘ └┘ └┘ └┘ └─┘ └───────┘ └┘ ┴
par └────┘ └┘ └┘ └┘ └─┘ └───────┘ └┘ ┴
pid └──┘ └┘ └┘ └┘ └─┘ └───────┘ └┘ ┴
st └─────────────┘└──┘└────────┘└───────────────────┘└────────┘┴
92
93 lemma exists_multiset_of_splits {f : polynomial α} : splits i f →
id └────────┘ ┴ └────┘ ┴ ┴
src └────────┘ └────┘
typ └────────┘ ┴ └────┘ ┴ ┴
doc └────────┘ └────┘
94 ∃ (s : multiset β), f.map i = C (i f.leading_coeff) *
id ┴ └──────┘ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴└────────────┘ ┴
src ┴ └──────┘ ┴ └──┘ ┴ ┴ └────────────┘ ┴
typ ┴ └──────┘ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴└────────────┘ ┴
doc └──────┘ └──┘ ┴ └────────────┘
95 (s.map (λ a : β, (X : polynomial β) - C a)).prod :=
id ┴└──┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ └──┘
src └──┘ ┴ └────────┘ ┴ ┴ └──┘
typ ┴└──┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ └──┘
doc └──┘ ┴ └────────┘ ┴ └──┘
96 suffices splits id (f.map i) → ∃ s : multiset β, f.map i =
id └────┘ └┘ ┴└──┘ ┴ ┴ └──────┘ ┴┴ ┴└──┘ ┴ ┴
src └────┘ └┘ └──┘ ┴ └──────┘ ┴ └──┘ ┴
typ └────┘ └┘ ┴└──┘ ┴ ┴ └──────┘ ┴┴ ┴└──┘ ┴ ┴
doc └────┘ └──┘ └──────┘ └──┘
97 (C (f.map i).leading_coeff) * (s.map (λ a : β, (X : polynomial β) - C a)).prod,
id ┴ ┴└──┘ ┴ └───────────┘ ┴ ┴└──┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ └──┘
src ┴ └──┘ └───────────┘ ┴ └──┘ ┴ └────────┘ ┴ ┴ └──┘
typ ┴ ┴└──┘ ┴ └───────────┘ ┴ ┴└──┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ └──┘
doc ┴ └──┘ └───────────┘ └──┘ ┴ └────────┘ ┴ └──┘
98 by rwa [splits_map_iff, leading_coeff_map i] at this,
id └────────────┘ └───────────────┘ ┴
src └───┘└────────────┘└┘└───────────────┘┴ └───────┘
typ └───┘└────────────┘└┘└───────────────┘┴┴└───────┘
doc └───┘ └┘ ┴ └───────┘
txt └───┘ └┘ ┴ └───────┘
par └───┘ └┘ ┴ └───────┘
pid └┘ └┘ ┴ ┴└──────┘
st └──────────────────┘└───────────────────┘┴└──────┘
99 is_noetherian_ring.irreducible_induction_on (f.map i)
id └─────────────────────────────────────────┘ ┴└──┘ ┴
src └─────────────────────────────────────────┘ └──┘
typ └─────────────────────────────────────────┘ ┴└──┘ ┴
doc └──┘
100 (λ _, ⟨{37}, by simp [is_ring_hom.map_zero i]⟩)
id ┴ ┴ └──────────────────┘ ┴
src ┴ └────┘└──────────────────┘┴ ┴
typ ┴ ┴ └────┘└──────────────────┘┴┴┴
doc └────┘└──────────────────┘┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴┴ ┴ ┴
st └────────────────────────────┘
101 (λ u hu _, ⟨0,
id ┴ └┘ ┴
typ ┴ └┘ ┴
102 by conv_lhs { rw eq_C_of_degree_eq_zero (is_unit_iff_degree_eq_zero.1 hu) };
id └────────────────────┘ └────────────────────────┘ └┘
src └─────────┘└─┘└────────────────────┘┴ └────────────────────────┘└─┘ └┘┴
typ └─────────┘└─┘└────────────────────┘┴ └────────────────────────┘└─┘└┘└┘┴
txt └─────────┘└─┘ ┴ └─┘ └┘┴
par └─────────┘└─┘ ┴ └─┘ └┘┴
pid ┴└───┘ ┴ └─┘ └─┘
st └─────────┘└───────────────────────────────────────────────────────────┘└┘└
103 simp [leading_coeff, nat_degree_eq_of_degree_eq_some (is_unit_iff_degree_eq_zero.1 hu)]⟩)
id └───────────┘ └─────────────────────────────┘ └────────────────────────┘ └┘
src └────┘└───────────┘└┘└─────────────────────────────┘┴ └────────────────────────┘└─┘ └┘
typ └────┘└───────────┘└┘└─────────────────────────────┘┴ └────────────────────────┘└─┘└┘└┘
doc └────┘└───────────┘└┘ ┴ └─┘ └┘
txt └────┘ └┘ ┴ └─┘ └┘
par └────┘ └┘ ┴ └─┘ └┘
pid ┴┴ └┘ ┴ └─┘ └┘
st ────────────────────────────────────────────────────────────────────────────────────────────┘
104 (λ f p hf0 hp ih hfs,
id ┴ ┴ └─┘ └┘ └┘ └─┘
typ ┴ ┴ └─┘ └┘ └┘ └─┘
105 have hpf0 : p * f ≠ 0, from mul_ne_zero hp.ne_zero hf0,
id ┴ ┴ ┴ ┴ └─────────┘ └┘└──────┘ └─┘
src ┴ ┴ └─────────┘ └──────┘
typ ┴ ┴ ┴ ┴ └─────────┘ └┘└──────┘ └─┘
st ┴
106 let ⟨s, hs⟩ := ih (splits_of_splits_mul _ hpf0 hfs).2 in
id └─┘ ┴ └┘ └──────────────────┘ └──┘ └─┘ ┴
src └──────────────────┘ ┴
typ └─┘ ┴ └┘ └──────────────────┘ └──┘ └─┘ ┴
107 ⟨-(p * norm_unit p).coeff 0 :: s,
id ┴ ┴ ┴ └───────┘ ┴ └───┘ └┘
src ┴ ┴ └───────┘ └───┘ └┘
typ ┴ ┴ ┴ └───────┘ ┴ └───┘ └┘
doc └───┘ └┘
108 have hp1 : degree p = 1, from hfs.resolve_left hpf0 hp (by simp),
id └────┘ ┴ ┴ └─┘└───────────┘ └──┘ └┘
src └────┘ ┴ └───────────┘ └──┘
typ └────┘ ┴ ┴ └─┘└───────────┘ └──┘ └┘ └──┘
doc └────┘ └──┘
txt └──┘
par └──┘
st └───┘
109 begin
st └─────
110 rw [multiset.map_cons, multiset.prod_cons, leading_coeff_mul, C_mul, mul_assoc,
id └───────────────┘ └────────────────┘ └───────────────┘ └───┘ └───────┘
src └──┘└───────────────┘└┘└────────────────┘└┘└───────────────┘└┘└───┘└┘└───────┘└─
typ └──┘└───────────────┘└┘└────────────────┘└┘└───────────────┘└┘└───┘└┘└───────┘└─
doc └──┘ └┘ └┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └┘ └┘ └─
par └──┘ └┘ └┘ └┘ └┘ └─
pid └┘ └┘ └┘ └┘ └┘ └─
st ────────────────────────────┘└──────────────────┘└─────────────────┘└─────┘└─────────┘└─
111 mul_left_comm (C f.leading_coeff), ← hs, ← mul_assoc, domain.mul_right_inj hf0],
id └───────────┘ ┴ └─────────────┘ └┘ └───────┘ └──────────────────┘ └─┘
src ─────────┘└───────────┘┴ ┴┴└─────────────┘└───┘ └──┘└───────┘└┘└──────────────────┘┴ ┴
typ ─────────┘└───────────┘┴ ┴┴└─────────────┘└───┘└┘└──┘└───────┘└┘└──────────────────┘┴└─┘┴
doc ─────────┘ ┴ ┴┴└─────────────┘└───┘ └──┘ └┘└──────────────────┘┴ ┴
txt ─────────┘ ┴ ┴ └───┘ └──┘ └┘ ┴ ┴
par ─────────┘ ┴ ┴ └───┘ └──┘ └┘ ┴ ┴
pid ─────────┘ ┴ ┴ └───┘ └──┘ └┘ ┴ ┴
st ──────────────────────────────────────────┘└────┘└───────────┘└────────────────────────┘└──
112 conv_lhs {rw eq_X_add_C_of_degree_eq_one hp1},
id └─────────────────────────┘ └─┘
src └────────┘└─┘└─────────────────────────┘┴ ┴
typ └────────┘└─┘└─────────────────────────┘┴└─┘┴
txt └────────┘└─┘ ┴ ┴
par └────────┘└─┘ ┴ ┴
pid ┴└──┘ ┴ ┴
st ─────────────────┘└────────────────────────────────┘└┘└
113 simp only [mul_add, coe_norm_unit hp.ne_zero, mul_comm p, coeff_neg,
id └─────┘ └───────────┘ └────────┘ └──────┘ ┴ └───────┘
src └─────────┘└─────┘└┘└───────────┘┴└────────┘└┘└──────┘┴ └┘└───────┘└─
typ └─────────┘└─────┘└┘└───────────┘┴└────────┘└┘└──────┘┴┴└┘└───────┘└─
doc └─────────┘ └┘ ┴ └┘ ┴ └┘ └─
txt └─────────┘ └┘ ┴ └┘ ┴ └┘ └─
par └─────────┘ └┘ ┴ └┘ ┴ └┘ └─
pid ┴└──┘└┘ └┘ ┴ └┘ ┴ └┘ └─
st ─────────────────────────────────────────────────────────────────────────────
114 C_neg, sub_eq_add_neg, neg_neg, coeff_C_mul, (mul_assoc _ _ _).symm, C_mul.symm,
id └───┘ └────────────┘ └─────┘ └─────────┘ └───────┘
src ─────────┘└───┘└┘└────────────┘└┘└─────┘└┘└─────────┘└┘ └───────┘└────────────┘ └─
typ ─────────┘└───┘└┘└────────────┘└┘└─────┘└┘└─────────┘└┘ └───────┘└────────────┘└────────┘└─
doc ─────────┘ └┘ └┘ └┘ └┘ └────────────┘ └─
txt ─────────┘ └┘ └┘ └┘ └┘ └────────────┘ └─
par ─────────┘ └┘ └┘ └┘ └┘ └────────────┘ └─
pid ─────────┘ └┘ └┘ └┘ └┘ └────────────┘ └─
st ───────────────────────────────────────────────────────────────────────────────────────────
115 mul_inv_cancel (show p.leading_coeff ≠ 0, from mt leading_coeff_eq_zero.1
id └────────────┘ └─────────────┘ ┴ └┘ └───────────────────┘
src ─────────┘└────────────┘┴ ┴└─────────────┘┴┴└───────┘└┘┴└───────────────────┘└──
typ ─────────┘└────────────┘┴ ┴└─────────────┘┴┴└───────┘└┘┴└───────────────────┘└──
doc ─────────┘ ┴ ┴└─────────────┘┴ └───────┘ ┴ └──
txt ─────────┘ ┴ ┴ ┴ └───────┘ ┴ └──
par ─────────┘ ┴ ┴ ┴ └───────┘ ┴ └──
pid ─────────┘ ┴ ┴ ┴ └───────┘ ┴ └──
st ────────────────────────────────────────────────────────────────────────────────────
116 hp.ne_zero), one_mul],
id └────────┘ └─────┘
src ───────────┘└────────┘└─┘└─────┘┴
typ ───────────┘└────────┘└─┘└─────┘┴
doc ───────────┘ └─┘ ┴
txt ───────────┘ └─┘ ┴
par ───────────┘ └─┘ ┴
pid ───────────┘ └─┘ ┴
st ────────────────────────────────┘└─
117 end⟩)
st ────────┘
118
119 section UFD
120
121 local attribute [instance, priority 10] principal_ideal_domain.to_unique_factorization_domain
id └───────────────────────────────────────────────────┘
src └───────────────────────────────────────────────────┘
typ └───────────────────────────────────────────────────┘
doc └───────────────────────────────────────────────────┘
122 local infix ` ~ᵤ ` : 50 := associated
id └────────┘
src └────────┘
typ └────────┘
123
124 open unique_factorization_domain associates
125
126 lemma splits_of_exists_multiset {f : polynomial α} {s : multiset β}
id └────────┘ ┴ └──────┘ ┴
src └────────┘ └──────┘
typ └────────┘ ┴ └──────┘ ┴
doc └────────┘ └──────┘
127 (hs : f.map i = C (i f.leading_coeff) * (s.map (λ a : β, (X : polynomial β) - C a)).prod) :
id ┴└──┘ ┴ ┴ ┴ ┴ ┴└────────────┘ ┴ ┴└──┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ └──┘
src └──┘ ┴ ┴ └────────────┘ ┴ └──┘ ┴ └────────┘ ┴ ┴ └──┘
typ ┴└──┘ ┴ ┴ ┴ ┴ ┴└────────────┘ ┴ ┴└──┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ └──┘
doc └──┘ ┴ └────────────┘ └──┘ ┴ └────────┘ ┴ └──┘
128 splits i f :=
id └────┘ ┴ ┴
src └────┘
typ └────┘ ┴ ┴
doc └────┘
129 if hf0 : f = 0 then or.inl hf0
id └┘ ┴ ┴ └────┘ └─┘
src └┘ ┴ └────┘
typ └┘ ┴ ┴ └────┘ └─┘
130 else
131 or.inr $ λ p hp hdp,
id └────┘ ┴ ┴ └┘ └─┘
src └────┘
typ └────┘ ┴ ┴ └┘ └─┘
132 have ht : multiset.rel associated
id └──────────┘ └────────┘
src └──────────┘ └────────┘
typ └──────────┘ └────────┘
doc └──────────┘
133 (factors (f.map i)) (s.map (λ a : β, (X : polynomial β) - C a)) :=
id └─────┘ ┴└──┘ ┴ ┴└──┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴
src └─────┘ └──┘ └──┘ ┴ └────────┘ ┴ ┴
typ └─────┘ ┴└──┘ ┴ ┴└──┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴
doc └──┘ └──┘ ┴ └────────┘ ┴
134 unique
id └────┘
src └────┘
typ └────┘
135 (λ p hp, irreducible_factors (mt (map_eq_zero i).1 hf0) _ hp)
id ┴ └┘ └─────────────────┘ └┘ └─────────┘ ┴ ┴ └─┘ └┘
src └─────────────────┘ └┘ └─────────┘ ┴
typ ┴ └┘ └─────────────────┘ └┘ └─────────┘ ┴ ┴ └─┘ └┘
136 (λ p, by simp [@eq_comm _ _ p, -sub_eq_add_neg,
id ┴ └─────┘ ┴
src └────┘ └─────┘└───┘ └──────────────────
typ ┴ └────┘ └─────┘└───┘┴└──────────────────
doc └────┘ └───┘ └──────────────────
txt └────┘ └───┘ └──────────────────
par └────┘ └───┘ └──────────────────
pid ┴┴ └───┘ └──────────────────
st └───────────────────────────────────────
137 irreducible_of_degree_eq_one (degree_X_sub_C _)] {contextual := tt})
id └──────────────────────────┘ └────────────┘ └┘
src ─────────┘└──────────────────────────┘┴ └────────────┘└───┘ └────────────┘└┘┴
typ ─────────┘└──────────────────────────┘┴ └────────────┘└───┘ └────────────┘└┘┴
doc ─────────┘ ┴ └───┘ └────────────┘ ┴
txt ─────────┘ ┴ └───┘ └────────────┘ ┴
par ─────────┘ ┴ └───┘ └────────────┘ ┴
pid ─────────┘ ┴ └──┘┴ └────────────┘ ┴
st ────────────────────────────────────────────────────────────────────────────┘
138 (associated.symm $ calc _ ~ᵤ f.map i :
id └─────────────┘ ┴└──┘ ┴
src └─────────────┘ └──┘
typ └─────────────┘ ┴└──┘ ┴
doc └──┘
139 ⟨(units.map' C : units β →* units (polynomial β)) (units.mk0 (f.map i).leading_coeff
id └────────┘ ┴ └───┘ ┴ └┘ └───┘ └────────┘ ┴ └───────┘ ┴└──┘ ┴ └───────────┘
src └────────┘ ┴ └───┘ └┘ └───┘ └────────┘ └───────┘ └──┘ └───────────┘
typ └────────┘ ┴ └───┘ ┴ └┘ └───┘ └────────┘ ┴ └───────┘ ┴└──┘ ┴ └───────────┘
doc └────────┘ ┴ └┘ └────────┘ └───────┘ └──┘ └───────────┘
140 (mt leading_coeff_eq_zero.1 (mt (map_eq_zero i).1 hf0))),
id └┘ └───────────────────┘┴ └┘ └─────────┘ ┴ ┴ └─┘
src └┘ └───────────────────┘┴ └┘ └─────────┘ ┴
typ └┘ └───────────────────┘┴ └┘ └─────────┘ ┴ ┴ └─┘
141 by conv_rhs {rw [hs, ← leading_coeff_map i, mul_comm]}; refl⟩
id └┘ └───────────────┘ ┴ └──────┘
src └────────┘└──┘ └──┘└───────────────┘┴ └┘└──────┘┴┴ └──┘
typ └────────┘└──┘└┘└──┘└───────────────┘┴┴└┘└──────┘┴┴ └──┘
doc └──┘
txt └────────┘└──┘ └──┘ ┴ └┘ ┴┴ └──┘
par └────────┘└──┘ └──┘ ┴ └┘ ┴┴ └──┘
pid ┴└───┘ └──┘ ┴ └┘ └┘
st └─────────┘└────┘└─────────────────────┘└────────┘ └┘└───┘
142 ... ~ᵤ _ : associated.symm (unique_factorization_domain.factors_prod (by simpa using hf0))),
id └─────────────┘ └──────────────────────────────────────┘ └─┘
src └─────────────┘ └──────────────────────────────────────┘ └──────────┘
typ └─────────────┘ └──────────────────────────────────────┘ └──────────┘└─┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid ┴└────┘
st └──────────────┘
143 let ⟨q, hq, hpq⟩ := exists_mem_factors_of_dvd (by simpa) hp hdp in
id └─┘ └┘ └───────────────────────┘ └┘ └─┘
src └───────────────────────┘ └───┘
typ └─┘ └┘ └───────────────────────┘ └───┘ └┘ └─┘
doc └───┘
txt └───┘
par └───┘
st └────┘
144 let ⟨q', hq', hqq'⟩ := multiset.exists_mem_of_rel_of_mem ht hq in
id └─┘ └─┘ └───────────────────────────────┘ └┘
src └───────────────────────────────┘
typ └─┘ └─┘ └───────────────────────────────┘ └┘
145 let ⟨a, ha⟩ := multiset.mem_map.1 hq' in
id └─┘ └──────────────┘┴
src └──────────────┘┴
typ └─┘ └──────────────┘┴
146 by rw [← degree_X_sub_C a, ha.2];
id └────────────┘ ┴ └┘
src └────┘└────────────┘┴ └┘ └─┘
typ └────┘└────────────┘┴┴└┘└┘└─┘
doc └────┘ ┴ └┘ └─┘
txt └────┘ ┴ └┘ └─┘
par └────┘ ┴ └┘ └─┘
pid └──┘ ┴ └┘ └─┘
st └─────────────────────┘└──┘└─┘└─
147 exact degree_eq_degree_of_associated (hpq.trans hqq')
id └────────────────────────────┘ └───────┘ └──┘
src └────┘└────────────────────────────┘┴ └───────┘┴ └─
typ └────┘└────────────────────────────┘┴ └───────┘┴└──┘└─
doc └────┘ ┴ ┴ └─
txt └────┘ ┴ ┴ └─
par └────┘ ┴ ┴ └─
pid ┴ ┴ ┴ ┴└
st ──────────────────────────────────────────────────────────
148
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
149 lemma splits_of_splits_id {f : polynomial α} : splits id f → splits i f :=
id └────────┘ ┴ └────┘ └┘ ┴ └────┘ ┴ ┴
src └────────┘ └────┘ └┘ └────┘
typ └────────┘ ┴ └────┘ └┘ ┴ └────┘ ┴ ┴
doc └────────┘ └────┘ └────┘
150 unique_factorization_domain.induction_on_prime f (λ _, splits_zero _)
id └────────────────────────────────────────────┘ ┴ ┴ └─────────┘
src └────────────────────────────────────────────┘ └─────────┘
typ └────────────────────────────────────────────┘ ┴ ┴ └─────────┘
151 (λ _ hu _, splits_of_degree_le_one _
id ┴ └┘ ┴ └─────────────────────┘
src └─────────────────────┘
typ ┴ └┘ ┴ └─────────────────────┘
152 ((is_unit_iff_degree_eq_zero.1 hu).symm ▸ dec_trivial))
id └────────────────────────┘┴ └┘ └──┘ ┴ └─────────┘
src └────────────────────────┘┴ └──┘ ┴ └─────────┘
typ └────────────────────────┘┴ └┘ └──┘ ┴ └─────────┘
doc └─────────┘
153 (λ a p ha0 hp ih hfi, splits_mul _
id ┴ ┴ └─┘ └┘ └┘ └─┘ └────────┘
src └────────┘
typ ┴ ┴ └─┘ └┘ └┘ └─┘ └────────┘
154 (splits_of_degree_eq_one _
id └─────────────────────┘
src └─────────────────────┘
typ └─────────────────────┘
155 ((splits_of_splits_mul _ (mul_ne_zero hp.1 ha0) hfi).1.resolve_left
id └──────────────────┘ └─────────┘ └┘┴ └─┘ └─┘ ┴ └──────────┘
src └──────────────────┘ └─────────┘ ┴ ┴ └──────────┘
typ └──────────────────┘ └─────────┘ └┘┴ └─┘ └─┘ ┴ └──────────┘
156 hp.1 (irreducible_of_prime hp) (by rw map_id)))
id └┘┴ └──────────────────┘ └┘ └────┘
src ┴ └──────────────────┘ └─┘└────┘
typ └┘┴ └──────────────────┘ └┘ └─┘└────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st └────────┘
157 (ih (splits_of_splits_mul _ (mul_ne_zero hp.1 ha0) hfi).2))
id └┘ └──────────────────┘ └─────────┘ └┘┴ └─┘ └─┘ ┴
src └──────────────────┘ └─────────┘ ┴ ┴
typ └┘ └──────────────────┘ └─────────┘ └┘┴ └─┘ └─┘ ┴
158
159 end UFD
160
161 lemma splits_iff_exists_multiset {f : polynomial α} : splits i f ↔
id └────────┘ ┴ └────┘ ┴ ┴ ┴
src └────────┘ └────┘ ┴
typ └────────┘ ┴ └────┘ ┴ ┴ ┴
doc └────────┘ └────┘
162 ∃ (s : multiset β), f.map i = C (i f.leading_coeff) *
id ┴ └──────┘ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴└────────────┘ ┴
src ┴ └──────┘ ┴ └──┘ ┴ ┴ └────────────┘ ┴
typ ┴ └──────┘ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴└────────────┘ ┴
doc └──────┘ └──┘ ┴ └────────────┘
163 (s.map (λ a : β, (X : polynomial β) - C a)).prod :=
id ┴└──┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ └──┘
src └──┘ ┴ └────────┘ ┴ ┴ └──┘
typ ┴└──┘ ┴ ┴ └────────┘ ┴ ┴ ┴ ┴ └──┘
doc └──┘ ┴ └────────┘ ┴ └──┘
164 ⟨exists_multiset_of_splits i, λ ⟨s, hs⟩, splits_of_exists_multiset i hs⟩
id └───────────────────────┘ ┴ ┴ └┘ └───────────────────────┘ ┴
src └───────────────────────┘ └───────────────────────┘
typ └───────────────────────┘ ┴ ┴ └┘ └───────────────────────┘ ┴
165
166 lemma splits_comp_of_splits (j : β → γ) [is_ring_hom j] {f : polynomial α}
id ┴ ┴ └─────────┘ ┴ └────────┘ ┴
src └─────────┘ └────────┘
typ ┴ ┴ └─────────┘ ┴ └────────┘ ┴
doc └─────────┘ └────────┘
167 (h : splits i f) : splits (λ x, j (i x)) f :=
id └────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
src └────┘ └────┘
typ └────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
doc └────┘ └────┘
168 begin
st └─────
169 change i with (λ x, id (i x)) at h,
id ┴ └┘ ┴
src └─────┘ └────┘ └──┘└┘┴ ┴ └─────┘
typ └─────┘┴└────┘ └──┘└┘┴ ┴┴ └─────┘
doc └─────┘ └────┘ └──┘ ┴ ┴ └─────┘
txt └─────┘ └────┘ └──┘ ┴ ┴ └─────┘
par └─────┘ └────┘ └──┘ ┴ ┴ └─────┘
pid ┴ └────┘ └──┘ ┴ ┴ └┘└───┘
st ───────────────────────────────────┘└─
170 rw [← splits_map_iff],
id └────────────┘
src └────┘└────────────┘┴
typ └────┘└────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid └──┘ ┴
st ─────────────────────┘└──
171 rw [← splits_map_iff i id] at h,
id └────────────┘ ┴ └┘
src └────┘└────────────┘┴ ┴└┘└────┘
typ └────┘└────────────┘┴┴┴└┘└────┘
doc └────┘ ┴ ┴ └────┘
txt └────┘ ┴ ┴ └────┘
par └────┘ ┴ ┴ └────┘
pid └──┘ ┴ ┴ ┴└───┘
st ──────────────────────────┘┴└───┘└─
172 exact splits_of_splits_id _ h
id └─────────────────┘ ┴
src └────┘└─────────────────┘└─┘ ┴
typ └────┘└─────────────────┘└─┘┴┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ───────────────────────────────┘
173 end
st └─┘
174
175 end splits
176
177 end polynomial